es:ES, i:Id, L:(IdLnk List), T:(IdType).
es-secret-server{table:ut2, encrypt:ut2, decrypt:ut2}
es-secret-server(es; T; L; i)
 (e1, e2:E.
 (lL.kind(e1) = rcv(lnk-inv(l),"encrypt")  Knd)
  (lL.kind(e2) = rcv(lnk-inv(l),"encrypt")  Knd)
  ((val(e1).2) = (val(e2).2)  Atom1)
  (e1 = e2)) 

latex

Definitions

let x,y,z = a in t(x;y;z), t.1, encrypt(tab;keyv), ptr(tab), ff, SQType(T), True, T, P  Q, P  Q, tt, if b then t else f fi , lnk(e), {T}, t.2, outl(x), next(tab), isl(x), Top, secret-table(T), P & Q, b, x. t(x), , t  T, "$x", P  Q, Id, x:A. B(x), lnk(k), rcv(l,tg), (e <loc e'), (state when e), s.x, e loc e' , P  Q, {i..j}, False, Unit, , , x(s), e@i. P(e), @i events of kind k change x to f State(ds) (val:T), A c B, state dsk:A sends [tg, e.f(e):B] on l, xL. P(x), let x = a in b(x), x:A. B(x), (xL.P(x)), es-secret-server, , x  {FDLNOr12445}

Lemmas

lnk wf, IdLnk sq, es-val wf, secret-table wf, ss-ptr-non-decreasing, ldst-inv, es-le-total, unit wf, st-next wf, isl wf, st-ptr-wf2, fpf-cap-single1, ss-atoms-distinct, es-first-init, es-loc-init, es-init wf, false wf, assert of le int, bnot of lt int, eqff to assert, bnot wf, le wf, le int wf, st-atom wf, assert of lt int, eqtt to assert, assert wf, iff transitivity, bool wf, st-length wf, st-ptr wf, lt int wf, data wf, int seg wf, es-vartype wf, Knd sq, es-loc-rcv, ldst wf, true wf, squash wf, lsrc-inv, lsrc wf, es-isrcv-loc, eqof eq btrue, id-deq wf, fpf-cap-single, es-kind-rcv, es-sender wf, es-when wf, event system wf, IdLnk wf, Id wf, es-secret-server wf, es-E wf, lnk-inv wf, rcv wf, es-kind wf, Knd wf, l exists wf, pi2 wf, nat wf